A, B:Type, f:(A(B + Top)), ds:(IdType), da:(IdKndType), X:Interface(ds;da;A), es:ES.
es-decl(es;ds;da)
 (e:{e:E| (e  [[interface-compose(f;X)]])} .
 [[interface-compose(f;X)]](e) = do-apply(f;[[X]](e))  B) 

latex

Definitions

AbsInterface(A), suptype(S; T), S  T, Top, e  X, do-apply(f;x), X(e), f o g  , , A c B, True, ff, if b then t else f fi , P  Q, P  Q, tt, p  q, P & Q, t  T, b, P  Q, x:A. B(x), A, False, Unit, ,

Lemmas

subtype rel sum, subtype rel function, btrue wf, assert of band, can-apply-compose-sq, can-apply wf, do-apply wf, es-interface-val wf, es-interface wf, top wf, Knd wf, Id wf, interface wf, event system wf, es-decl wf, es-E wf, inconsistent-bool-eq, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, abs-interface wf, es-is-interface wf, eqtt to assert, bool wf, is-interface-compose, abs-interface-compose